package jtg.generator;

import com.alibaba.fastjson.JSON;
import fj.P;
import jtg.generator.bean.ConverJimpleVar;
import jtg.graphics.SootCFG;
import jtg.solver.ExpressionException;
import jtg.solver.Z3Solver;
import jtg.visualizer.Visualizer;
import soot.*;
import soot.jimple.NewArrayExpr;
import soot.jimple.StaticFieldRef;
import soot.jimple.internal.*;
import soot.toolkits.graph.UnitGraph;

import java.io.File;
import java.lang.reflect.Field;
import java.util.*;

public abstract class BaseGenerator {

    protected String clsPath;
    protected String clsName;
    protected String mtdName;
    // 原控制流图
    protected UnitGraph ug;
    // 扩展后的控制流图
    protected UnitGraph expandUg;
    protected Body body;
    // 调用的语句
    protected Set<Unit> invokes = new HashSet<>();

    protected List<Unit> heads;
    protected List<Unit> tails;
    // 某种覆盖准则下的路径集合
    protected Set<List<Unit>> pathSet;
    protected Set<List<Unit>> solvedPath;
    // 无解的路径，记一下他的约束条件
    protected Map<List<Unit>, String> insolublePath;
    protected Map<String, Type> typeSwitch;

    protected List<Local> localPara;
    // 出现强制类型转换的变量
    private ArrayList<ConverJimpleVar> converJimpleVars = new ArrayList<>();

    public BaseGenerator(String classPath, String className, String methodName) {
        String defaultClsPath = System.getProperty("user.dir") + File.separator + "target" + File.separator + "classes";
        if (classPath != null && !classPath.equals("")) clsPath = classPath;
        else clsPath = defaultClsPath;
        clsName = className;
        mtdName = methodName;
        // 获取对应方法的活动方法体（Soot里的类）
        body = SootCFG.getMethodBody(clsPath, clsName, mtdName);
        // 获取完整的控制流图。UnitGraph类
        ug = SootCFG.getMethodCFG(clsPath, clsName, mtdName);
        // 扩展控制流图
        SootCFG.expandCFG(body, invokes);
        // 扩展后的控制流图
        expandUg = SootCFG.getMethodCFG(body);
    }

    public void drawCFG(String graphName, boolean indexLabel) {
        Visualizer.printCFGDot(graphName, ug, indexLabel);
        Visualizer.printCFGDot("expand_"+graphName, expandUg, indexLabel);
    }

    public String getClsName() {
        return clsName;
    }

    public String getMtdName() {
        return mtdName;
    }

    public List<Local> getLocalPara() {
        return localPara;
    }

    /**
     * 识别并返回给定方法体中的 Jimple 特有的局部变量。
     * 通常用于表示在字节码级别捕获的中间值或操作数。
     * 不是特有的局部变量：与Java源代码中的变量一一对应。可以是方法参数、类成员变量或临时变量等
     * 在某些情况下，分析 Jimple 特有的局部变量可能对于理解程序的结构和执行过程是有帮助的。
     * @return
     */

    private List<Local> getParJVars() {
        //Jimple自身增加的Locals，不是被测代码真正的变量
        ArrayList<Local> jimpleVars = new ArrayList<Local>();
        for (Local l : body.getLocals()) {
            // 对于每个局部变量，检查其字符串表示形式是否以 $ 开头。
            // 如果是，说明这是 Jimple 特有的局部变量，将其添加到 jimpleVars 列表中。
            if (l.toString().startsWith("temp$")) {
//            if (l.toString().contains("$")) {
                jimpleVars.add(l);
            }
        }
        return jimpleVars;
    }

    /**
     * 获取方法的参数
     */
    private List<Local> getParameter() {
        ArrayList<Local> paras = new ArrayList<Local>();
        for (Local para : body.getParameterLocals()) {
            paras.add(para);
//            System.out.print(para.toString());
        }
//        System.out.println();
        return paras;
    }

    protected void initialize(){
        localPara = getParameter();
        heads = ug.getHeads();
        tails = ug.getTails();
        // 在具体的覆盖准则下需要填充具体的内容
        pathSet = new HashSet<>();
        typeSwitch = new HashMap<>();
        solvedPath = new HashSet<>();
        insolublePath = new HashMap<>();
    };

    /**
     * 主要方法,生成测试用例
     * 注意这个BaseGenerator里面没有对pathSet进行填充
     * 每一个子类都需要在initialize函数里填充其要生成测试用例的路径
     * @return
     */
    public List<String> generate() {
        initialize();
        drawCFG("graph", true);
        calCompletePath();
        // 存储生成的测试用例
        ArrayList<String> testSet = new ArrayList<>();
        ArrayList<String> testFinalSet = new ArrayList<>();
        // 先记一下JIdentityStmt的类型，方便最后解出测试集合之后转到对应类型
        for (Unit unit : body.getUnits()) {
            if (unit instanceof JIdentityStmt) {
                JIdentityStmt jIdentityStmt = (JIdentityStmt) unit;
                String leftStr = jIdentityStmt.getLeftOp().toString();
                Type type = jIdentityStmt.getRightOp().getType();
                typeSwitch.put(leftStr, type);
            } else
                break; // 因为JIdentityStmt只在最前面一起出现
        }
        // 为每条路径生成测试数据
        for (List<Unit> path : pathSet) {
            // 如果这条路径已经解过、生成过了，直接跳过
            if (solvedPath.contains(path)) continue;
//            // 先找到整条路径，因为如基路径有的不完整
//            Set<List<Unit>> completePath = calCompletePath(path);
            System.out.println("The path is: " + path.toString());
//            boolean solvedOrNot = false;
            try {
                String pathConstraint = calPathConstraint(path);
                // 好聪明！因为Java基本类型对其具体值都是有一些约束的。但是Z3求解器把他们全都当作Real来处理，
                // 所以给对应的类型加一些对应的约束，就能限制住它在类型的可取值范围内取值
                pathConstraint = addTypeConstraint(pathConstraint);
                System.out.println("The corresponding path constraint is: " + pathConstraint);
                //如果路径约束为空字符串，表示路径约束为恒真，直接随机生成
                if (pathConstraint.isEmpty()) {
                    RandomGenerator randomGenerator = new RandomGenerator(clsPath, clsName, mtdName);
                    String result = JSON.toJSONString(randomGenerator.generate());
                    testSet.add(result);
                    testFinalSet.add(result);
                }
                else {
                    String solution = solve(pathConstraint);
                    if (solution.equals("") || solution.isEmpty()) {
                        // 路径约束是恒真式子
                        solvedPath.add(path);
                        RandomGenerator randomGenerator = new RandomGenerator(clsPath, clsName, mtdName);
                        String result = JSON.toJSONString(randomGenerator.generate());
                        testSet.add(result);
                        testFinalSet.add(result);
                    } else if (solution.contains("无解")) {
                        System.out.println("该路径无解：" + path.toString());
                        insolublePath.put(path, pathConstraint);
                        continue;
                    }else {
                        // 多处理一环，得到最终结果，如类型转换、字符串长度等等
                        solvedPath.add(path);
                        testSet.add(solution);
                        System.out.println(solution);
                        solution = DealSolution.dealSolution(solution, localPara);
                        testFinalSet.add(solution);
                    }
                }
            } catch (Exception e) {
                e.printStackTrace();
            }
        }

        // 生成的测试用例非空，输出一下
        if (!testSet.isEmpty()) {
            System.out.println();
            System.out.println("(一)生成的测试用例输入The generated test case inputs:");
            int count = 1;
            for (int i = 0; i < testSet.size(); i++) {
                String tc = testSet.get(i);
                String finalTc = testFinalSet.get(i);
                System.out.println("( " + count + " ) " + tc.toString());
                System.out.println("对应最终数据:( " + count + " ) " + finalTc.toString());
                count++;
            }
            System.out.println("(二)无解的路径：");
            // 输出一下无解的路径
            int insoluCount = 1;
            for (List<Unit> key : insolublePath.keySet()) {
                System.out.println("( " + insoluCount + " ) " + "路径约束是：" + insolublePath.get(key));
                System.out.println("对应路径是：" + key);
            }
            // 输出一下覆盖率
            int totPathNum = pathSet.size();
            int soveledPaNum = solvedPath.size();
            String covRate = String.format("%.2f", 100.0 * (double) soveledPaNum / (double) totPathNum);
            System.out.println("给定的路径共有" + totPathNum + "条，我们生成的测试用例能够覆盖" + soveledPaNum +"条，覆盖率：" + covRate);
        }else {
            System.out.println("一条测试数据也没生成？！");
        }
        System.out.println();
        return testSet;
    }

    /**
     * 要填充pathSet,填充什么取决于使用何种覆盖准则
     */
    protected abstract void calCompletePath();


    private List<List<Unit>> getAllPath() {
        return null;
    }

    /**
     * 计算给定路径的路径约束
     *
     * @param path 包含单元（语句）的路径
     * @return 路径约束的字符串表示
     */
    public String calPathConstraint(List<Unit> path) {

        // 初始化路径约束和预期结果
        String pathConstraint = "";
        String expectedResult;

        // 用于存储赋值语句的哈希映射，也用于中间变量的消除
        HashMap<String, String> assignList = new HashMap<>();
        // 存储带有Jimple变量的条件
        ArrayList<String> stepConditionsWithJimpleVars = new ArrayList<String>();
        // 存储条件
        ArrayList<String> stepConditions;

        // 遍历路径中的每个单元（语句）
        for (Unit stmt : path) {
            // 调用语句，已经展开了，这里直接跳过
            if (invokes.contains(stmt)) continue;
            // 赋值语句
            if (stmt instanceof JAssignStmt) {
                // 要处理一下有类型转换的局部变量，将语句中的类型转换去掉，然后把他存起来
                JAssignStmt jAssignStmt = (JAssignStmt) stmt;
                // 处理左边和右边，包括有复杂类型的局部变量
                try{
                    dealAssign(jAssignStmt, assignList);
                }catch (Exception e) {
                    e.printStackTrace();
                }
                continue;
            }
            // 条件语句
            if (stmt instanceof JIfStmt) {
                // 条件
                String ifstms = ((JIfStmt) stmt).getCondition().toString();
                // 循环发现的问题，条件里的变量每次都要先进行赋值，因为在过程中是会变的
                // 条件里的变量进行赋值
                String[] ifConSplit = ifstms.toString().split("\\s+");
                StringBuffer aftAssignCon = new StringBuffer();
                for (String s : ifConSplit) {
                    aftAssignCon.append(Optional.ofNullable(assignList.get(s)).orElse(s) + " ");
                }
                ifstms = aftAssignCon.toString();
                // 下一条语句的索引
                int nextUnitIndex = path.indexOf(stmt) + 1;
                Unit nextUnit = path.get(nextUnitIndex);

                //如果ifstmt的后继语句（getTarget）不是ifstmt中goto语句，说明ifstmt中的条件为假
                if (!((JIfStmt) stmt).getTarget().equals(nextUnit))
                    ifstms = "!( " + ifstms + " )";
                else
                    ifstms = "( " + ifstms + " )";
                // WithJimpleVars并非是特有变量
                stepConditionsWithJimpleVars.add(ifstms);
                continue;
            }
            // switch语句
            if (stmt instanceof JTableSwitchStmt) {
                JTableSwitchStmt switchStmt = (JTableSwitchStmt) stmt;
                // 获取switch语句的条件值
                Value conditionValue = switchStmt.getKey();
                String condition = conditionValue.toString();
                // 将条件值进行赋值替换
                String[] conditionSplit = condition.split("\\s+");
                StringBuilder afterAssignCondition = new StringBuilder();
                for (String s : conditionSplit) {
                    afterAssignCondition.append(Optional.ofNullable(assignList.get(s)).orElse(s)).append(" ");
                }
                condition = afterAssignCondition.toString();
                // 下一条语句的索引
                int nextUnitIndex = path.indexOf(stmt) + 1;
                Unit nextUnit = path.get(nextUnitIndex);
                // 比较哪一个condition对应下一条语句
                // 如果对应default的target
                if (nextUnit.equals(switchStmt.getDefaultTarget())) {
                    // 这里是由于switch语句的getIndex得到的index和枚举类型中的差了1
                    int j = switchStmt.getHighIndex();
                    condition = "( " + condition + "= " + j + " )";
                    stepConditionsWithJimpleVars.add(condition);
                    continue;
                }
                for (int j = switchStmt.getLowIndex(); j <= switchStmt.getHighIndex(); j++){
                    // 如果是这一条语句，找到对应的条件，注意这里index和target的index有点不对应，差一
                    if (switchStmt.getTarget(j-1).equals(nextUnit)) {
                        condition = "( " + condition + "= " + j + "-1 )";
                        break;
                    }
                }
                stepConditionsWithJimpleVars.add(condition);
                continue;
            }
            // 返回语句，但是没用到
            if (stmt instanceof JReturnStmt) {
                expectedResult = stmt.toString().replace("return", "").trim();
            }
        }
        System.out.println("The step conditions with JimpleVars are: " + stepConditionsWithJimpleVars);

        // 获取已经除去Jimple特有变量的路径约束
        stepConditions = replaceJvars(assignList, stepConditionsWithJimpleVars);

        // 一路上没有条件，路径约束就是空的
        if (stepConditions.isEmpty())
            return "";
        // 获取第一个条件
        pathConstraint = stepConditions.get(0);
        int i = 1;
        while (i < stepConditions.size()) {
            // 把所有条件用‘&&’连起来
            pathConstraint = pathConstraint + " && " + stepConditions.get(i);
            i++;
        }
        // 返回约束
        //System.out.println("The path expression is: " + pathConstraint);
        return pathConstraint;
    }

    // 处理强制类型转换
    private void dealAssign(JAssignStmt stmt, HashMap<String, String> assignList) throws Exception {
        Value rightOp = stmt.getRightOp();
        Value leftOp = stmt.getLeftOp();
        String right = rightOp.toString();
        String left = leftOp.toString();
        String dealtRight = right;
        String dealtLeft = leftOp.toString();

        // 处理赋值语句的右边
        // 对赋值语句先进行一个处理
        if (rightOp instanceof JimpleLocal) {
            // 如果是普通局部变量，有可能是中间变量，那就把它改成具体的值（assignList中有存
            dealtRight = Optional.ofNullable(assignList.get(right)).orElse(right);
        } else if (rightOp instanceof JLengthExpr) {
            // 如果含有数组长度(包括字符串长度),处理长度表达式
            JLengthExpr jLengthExpr = (JLengthExpr) rightOp;
            Value op = jLengthExpr.getOp(); //lengthof op
            dealtRight = Optional.ofNullable(assignList.get(op.toString())).orElse(op.toString()) + "_len";
            typeSwitch.put(dealtRight, IntType.v()); //长度类型是整型
        }else if (rightOp instanceof JInstanceFieldRef) {
            // 如果是调用的其他实例中的字段
            JInstanceFieldRef jInstanceFieldRef = (JInstanceFieldRef) rightOp;
            // 先获取这个实例所属的实例的名字
            String baseClsName = Optional.ofNullable(assignList.get(jInstanceFieldRef.getBase().toString())).orElse(jInstanceFieldRef.getBase().toString());
            // 看看这个实例是不是一个局部变量，如果是的话，要避免覆盖掉已经写进去的赋值
            if (baseClsName.contains("newObj_")) {
                return;
            }else {
                dealtRight = baseClsName + "_" + jInstanceFieldRef.getField().getName();
                typeSwitch.put(dealtRight, rightOp.getType());
            }
        } else if (rightOp instanceof JArrayRef) {
            // 处理数组类型
            JArrayRef jArrayRef = (JArrayRef) rightOp;
            // 调用的数组是哪个，如果是中间变量要替换成最初始的名字
            String arrStr = jArrayRef.getBase().toString();
            arrStr = Optional.ofNullable(assignList.get(arrStr)).orElse(arrStr);
            // 调用的哪一个元素
            String indexStr = jArrayRef.getIndex().toString();
            indexStr = Optional.ofNullable(assignList.get(indexStr)).orElse(indexStr);
            // TODO:索引中有其他变量的不行
            // 改一下名字，方便后面处理：arr_i0/i1/...
            // 注意这里处理switch，因为soot把switch语句当成了一个int数组变量，这里要额外处理它，把switchArr_iXX_ordinal直接变成XX
            // 方便后面处理
            if (arrStr.contains("switchArr"))
                dealtRight = indexStr.substring(0, indexStr.indexOf("_"));
            else dealtRight = arrStr + "_i" + indexStr;
        } else if (rightOp instanceof AbstractJimpleFloatBinopExpr) {
            // 发现z3要求解带符号的和被赋成 a */+/-/... b 的变量，必须要加上括号
            //最后正式在处理变量的具体表示，如：r0 = r1 + r2
            StringBuilder detailRightOp = new StringBuilder();
            String[] split = right.split("\\s+");
            split[0] = " ( " + Optional.ofNullable(assignList.get(split[0])).orElse(split[0]) + " ) ";
            split[2] = " ( " + Optional.ofNullable(assignList.get(split[2])).orElse(split[2]) + " ) ";
            if (split[0].startsWith(" ( -")) split[0] = split[0].replace(" ( -", " ( 0 -");
            if (split[2].startsWith(" ( -")) split[2] = split[2].replace(" ( -", " ( 0 -");
            for (String s : split) {
                detailRightOp.append(s); //将右侧的语句化简成最简单
            }
            dealtRight = detailRightOp.toString();
        }else if (rightOp instanceof JNegExpr) {
            JNegExpr jNegExpr = (JNegExpr) rightOp;
            String opStr = jNegExpr.getOp().toString();
            opStr = Optional.ofNullable(assignList.get(opStr)).orElse(opStr);
            dealtRight = " ( 0 - " + opStr + " ) ";
        } else if (rightOp instanceof StaticFieldRef) {
            // 对静态字段的处理，主要是处理枚举类型
            StaticFieldRef staticFieldRef = (StaticFieldRef) rightOp;
            // 拿到静态字段的soot类型
            Class typeClass = staticFieldRef.getType().getClass();
//            String type = staticFieldRef.getType().getClass().getName();
            // 先判定这个是不是Java对switch语句的处理
            if (typeClass.getName().equals("soot.ArrayType")) {
                // 暂时只处理了switch（soot多加了一个数组来处理他），不知道有没有别的
                dealtRight = "switchArr";
            } else if (typeClass.getName().equals("soot.RefType")) {
                // 使用Java的反射机制
                // getType静态字段的类型
                Class<?> cls = Class.forName(staticFieldRef.getType().toString());
                // 把cls换成具体引用的那个枚举类型，DeclaringClass：包含的静态字段的类的名字
//                cls = Class.forName(staticFieldRef.getField().getDeclaringClass().toString());
                if (cls.isEnum()) {
                    // 引用的枚举类型
                    Field field = cls.getDeclaredField(staticFieldRef.getField().getName());
                    // 通过反射获取静态字段的值，由于静态字段属于类而不是对象，因此传递 null 作为参数。
                    Enum anEnum = (Enum) field.get(null);
                    // 获取枚举常量的序号
                    int ordinal = anEnum.ordinal();
                    dealtRight = String.valueOf(ordinal);
                }
            }
        }
        else if (rightOp instanceof JCastExpr) {
            // 如果含有强制类型
            JCastExpr jCastExpr = (JCastExpr) rightOp;
            String originalType = jCastExpr.getOp().getType().toString();
            // new一个强制类型转换类
            ConverJimpleVar converJimpleVar = new ConverJimpleVar();
            // 其他的没处理
            if (originalType.equals("int") || originalType.equals("float") || originalType.equals("double")
                    || originalType.equals("java.lang.Byte")
                    || originalType.equals("short") || originalType.equals("boolean") || originalType.equals("long")
                    || originalType.equals("char") || originalType.equals("byte")
                    || originalType.equals("java.lang.Object") || originalType.equals("java.lang.String")) {
                    if (localPara.contains(jCastExpr.getOp())) {
                        converJimpleVar.setOriginalType(originalType);
                        converJimpleVar.setSwichType(jCastExpr.getCastType().toString());
                        converJimpleVar.setVar(jCastExpr.getOp().toString());
                        converJimpleVars.add(converJimpleVar);
                        // 找到强制类型转换的字符串
                        int lParenthesis = right.indexOf("(");
                        int rParenthesis = matchBracket(right, lParenthesis);
                        dealtRight = right.replace(right.substring(lParenthesis, rParenthesis+1), "").trim();
                        dealtRight = Optional.ofNullable(assignList.get(dealtRight)).orElse(dealtLeft);
                    } else {
//                        throw new ExpressionException("强制转换：不是参数的变量的强制转换");
                        // 先直接不管这个类型转换
                        int lParenthesis = right.indexOf("(");
                        int rParenthesis = matchBracket(right, lParenthesis);
                        dealtRight = right.replace(right.substring(lParenthesis, rParenthesis+1), "").trim();
                        dealtRight = Optional.ofNullable(assignList.get(dealtRight)).orElse(dealtRight);
                    }
                }else {
//                throw new ExpressionException("强制转换：没处理的类型");
            }
        } else if (rightOp instanceof JInstanceOfExpr) {
            // 如果是XX instanceof XX类型 这种语句，弄一个类型转换
            JInstanceOfExpr jInstanceOfExpr = (JInstanceOfExpr) rightOp;
            System.out.println(jInstanceOfExpr.getOp().getType());
            typeSwitch.put(jInstanceOfExpr.getOp().toString(), jInstanceOfExpr.getType());
            return;
        } else if (rightOp instanceof JCmplExpr) {
            // 无符号整数比较
            JCmplExpr jCmplExpr = (JCmplExpr) rightOp;
            String subLOp = jCmplExpr.getOp1().toString();
            String subROp = jCmplExpr.getOp2().toString();
            subLOp = Optional.ofNullable(assignList.get(subLOp)).orElse(subLOp);
            subROp = Optional.ofNullable(assignList.get(subROp)).orElse(subROp);
            dealtRight = subLOp + " - " + subROp;
        } else if (rightOp instanceof JCmpExpr) {
            // 带符号比较
            JCmpExpr jCmpExpr = (JCmpExpr) rightOp;
            String subLOp = jCmpExpr.getOp1().toString();
            String subROp = jCmpExpr.getOp2().toString().replace("L", "");
            subLOp = Optional.ofNullable(assignList.get(subLOp)).orElse(subLOp);
            subROp = Optional.ofNullable(assignList.get(subROp)).orElse(subROp);
            dealtRight = subLOp + " - " + subROp;
        } else if (rightOp instanceof JNewExpr) { //new 对象
            JNewExpr jNewExpr = (JNewExpr) rightOp;
            String rightOpStr = "newObj_" + jNewExpr.getBaseType();
            dealtRight = rightOpStr.replace(".", "_"); //jtg.Student改成(jtg_Student) jtgPerson
        }
        else if (rightOp instanceof NewArrayExpr) {
            // 实现带局部变量的
            JNewArrayExpr jNewArrayExpr = (JNewArrayExpr) rightOp;
            // 先把这个new一个数组改掉，不然z3说非法字符（newArr_type），后面会被放入assignList
            dealtRight = "newArr_" + jNewArrayExpr.getBaseType().toString();
            // 把新数组的长度放进assignList
            String leftConcrete = Optional.ofNullable(assignList.get(left)).orElse(left);
            assignList.put(leftConcrete + "_len", jNewArrayExpr.getSize().toString());
        } else dealtRight = Optional.ofNullable(assignList.get(right)).orElse(right);

        // 再处理左边
        if (leftOp instanceof JInstanceFieldRef) {
            // 如果是调用的其他实例中的字段
            JInstanceFieldRef jInstanceFieldRef = (JInstanceFieldRef) leftOp;
            // 先获取这个实例所属的类名字
            String baseClsName = Optional.ofNullable(assignList.get(jInstanceFieldRef.getBase().toString())).orElse(jInstanceFieldRef.getBase().toString());
            dealtLeft = baseClsName + "_" + jInstanceFieldRef.getField().getName();
        } else if (leftOp instanceof JArrayRef) {
            // 处理数组类型
            JArrayRef jArrayRef = (JArrayRef) leftOp;
            // 调用的数组是哪个，如果是中间变量要替换成最初始的名字
            String arrStr = jArrayRef.getBase().toString();
            arrStr = Optional.ofNullable(assignList.get(arrStr)).orElse(arrStr);
            // 调用的哪一个元素
            String indexStr = jArrayRef.getIndex().toString();
            indexStr = Optional.ofNullable(assignList.get(indexStr)).orElse(indexStr);
            // TODO:索引中有其他变量的不行
            // 可能是一个式子，先求解一下？
            // 改一下名字，方便后面处理：arr_i0/i1/...
            // 注意这里处理switch，因为soot把switch语句当成了一个int数组变量，这里要额外处理它，把switchArr_iXX_ordinal直接变成XX
            // 方便后面处理
            if (arrStr.contains("switchArr"))
                dealtLeft = indexStr.substring(0, indexStr.indexOf("_"));
            else dealtLeft = arrStr + "_i" + indexStr;
        }
        assignList.put(dealtLeft, dealtRight);
    }

    // 处理所有语句中Jimple自定义的临时变量
    private ArrayList<String> replaceJvars(HashMap<String, String> assignList, ArrayList<String> stepConditionsWithJimpleVars) {
        // 结果：路径约束条件
        ArrayList<String> stepConditions = new ArrayList<>();
        // 获取特有的Jimple变量
        List<Local> jVars = getParJVars();

        //bug 没有考虑jVars（特有变量）为空的情况
        if (jVars.size() != 0) {
            // 对条件语句的处理
            for (int i = 0; i < stepConditionsWithJimpleVars.size(); i++) {
                String cond = stepConditionsWithJimpleVars.get(i);
                //替换条件里特有的Jimple变量
                for (Local lv : jVars) {
                    // 如果包含特有变量
                    if (cond.contains(lv.toString())) {
                        // 把特有变量具体的值替换进去
                        cond = cond.replace(lv.toString(), assignList.get(lv.toString()).trim());
                    }//不包含特有变量的条件呢？？？
//                    else stepConditions.add(cond);
                }
                if (cond.contains("$SwitchMap")) {
                    int leftJBrac = cond.indexOf('<');
                    int rightJBrac = matchBracket(cond, leftJBrac);
                    cond = cond.replace(cond.substring(leftJBrac, rightJBrac+3), "");
                }
                stepConditions.add(cond);
            }
        } else {
//            // 对switch语句的处理
//            for (int i = 0; i < stepConditionsWithJimpleVars.size(); i++) {
//                String cond = stepConditionsWithJimpleVars.get(i);
//                if (cond.contains("$SwitchMap")) {
//                    int leftJBrac = cond.indexOf('<');
//                    int rightJBrac = matchBracket(cond, leftJBrac);
//                    cond = cond.replace(cond.substring(leftJBrac, rightJBrac+3), "");
//                }
//                stepConditions.add(cond);
//            }
            stepConditions = stepConditionsWithJimpleVars;
        }
        return stepConditions;
    }

    // 匹配括号，无论是圆括号还是尖括号
    private int matchBracket(String waitDetectStr, int lBracketsIndex) {
        int rBracketsIndex = -1;

        // 检测传进来的左括号索引是否超出
        if (waitDetectStr.length() > lBracketsIndex) {
            // 检测传进来的索引对应的字符是否为左括号
            if ('(' == waitDetectStr.charAt(lBracketsIndex)) {
                // 获取另一配对括号位置
                int count = 1;
                for (int i = lBracketsIndex + 1; i < waitDetectStr.length(); i++) {
                    if (waitDetectStr.charAt(i) == '(') {
                        count++;
                    } else if (waitDetectStr.charAt(i) == ')') {
                        count--;
                    }
                    if (count == 0) {
                        rBracketsIndex = i;
                        break;
                    }
                }
            }else if ('<' == waitDetectStr.charAt(lBracketsIndex)) {
                // 获取另一配对括号位置
                int count = 1;
                for (int i = lBracketsIndex + 1; i < waitDetectStr.length(); i++) {
                    if (waitDetectStr.charAt(i) == '<') {
                        count++;
                    } else if (waitDetectStr.charAt(i) == '>') {
                        count--;
                    }
                    if (count == 0) {
                        rBracketsIndex = i;
                        break;
                    }
                }
            }
        }
        return rBracketsIndex;
    }

    private String addTypeConstraint(String oldConstraint) throws ClassNotFoundException {
        String constraint = new String(oldConstraint);
        if (oldConstraint.equals("")) oldConstraint = "1 == 1";
        for (Map.Entry<String, Type> stringTypeEntry : typeSwitch.entrySet()) {
            String val = stringTypeEntry.getKey();
            Type type = stringTypeEntry.getValue();
            if (constraint.contains(val)) {
                if (type instanceof IntType) {
                    oldConstraint = oldConstraint + " && ( " + val + " % 1 = 0 )";
                } else if (type instanceof CharType) {
                    oldConstraint = oldConstraint + " && ( " + val + " % 1 = 0 ) && ( " + val + " >= 0 ) && ( " + val + " <= 65535 )";
                } else if (type instanceof BooleanType) {
                    oldConstraint = oldConstraint + " && ( " + val + " = 0 || " + val + " = 1 )"; //0 true
                } else if (type instanceof ArrayType) {
                    ArrayType arrayType = (ArrayType) type;
                    Type elementType = arrayType.getElementType();
                } else if (type instanceof RefType) {
                    Class<?> clz = Class.forName(type.toString());
                    if (clz.isEnum()) {
                        Class<Enum> clazz = (Class<Enum>) clz;
                        int ordNum = clazz.getEnumConstants().length;
                        oldConstraint = oldConstraint + " && ( " + val + " % 1 = 0 ) && ( " + val + " >= 0 ) && ( " + val + " < " + ordNum + " )";
                    }
                }
//                System.out.println(type.getClass().getSimpleName() + " haha ");
            }
        }
        return oldConstraint;
    }

    public String solve(String pathConstraint) throws Exception {
        // 处理的带引号的字符串
        String[] pathCons = pathConstraint.split("&&");
//        StringBuffer solvableCon = new StringBuffer();
//        StringBuffer unsolvableCon = new StringBuffer();
        for (int i = 0; i < pathCons.length; i++) {
            String pathCon = pathCons[i];
            if (pathCon.contains("\"")) {
                boolean dealt = false;
                String[] items = pathCon.split("\\s+");
                for (String item : items) {
                    // 如果是长度，即item是"xxx"_value_len的形式
                    if (item.contains("\"") && item.contains("_value_len")) {
                        int firstIndex = item.indexOf('\"');
                        int lastIndex = item.lastIndexOf('\"');
                        // "xxx"中xxx的长度
                        int len = item.substring(firstIndex + 1, lastIndex).length();
                        pathConstraint = pathConstraint.replace(item, String.valueOf(len));
                        dealt = true;
                        break;
                    }
                }
                if (dealt == false) throw new ExpressionException("涉及到string其他函数了，无法处理");
                else break;
            }
        }
        return Z3Solver.solve(pathConstraint, converJimpleVars);
        // 直接用z3来解析
//        return unsolvableCon.toString() + Z3Solver.solve(solvableCon.toString(), converJimpleVars);
    }

    // 随机生成一条测试语句 **=**
    public String randomTC(List<Local> parameters) {

        String varName;
        String varValue = "";
        String testinput = "";

        for (Local para : parameters) {
            varName = para.getName();
            if ("int".equals(para.getType().toString())) {
                varValue = String.valueOf((int)(Math.random() * 10));
            }
            if ("String".equals(para.getType().toString())) {
                varValue = "abc";
            }
            //其它的基本类型没写
            // 要实现的！！！！！！！！！
            testinput = testinput + " " + varName + "=" + varValue;
        }
        return testinput;
    }

}
